SMT Solver 개념
리버싱 과정에서 복잡한 수학 공식을 이용해서 리버싱을 어렵게 만듭니다. SMT Solver는 이런 리버싱 과정에서 복잡하게 얽힌 수학 공식을 자동으로 계산해주는 도구입니다.
SAT(Boolean SAtisfiability Problem) - 충족 가능성 문제
- 참/거짓 불리언 값을 가질 수 있는 변수들이 논리 연산 AND, OR, NOT으로 연결되었을 때, 전체 식을 참으로 만드는 변수를 찾는 문제를 말한다.
if((a && !b) && (b || c) && (c && a)) {
printf("Correct!\n");
}